Process Analysis Toolkit (PAT) 3.5 Help |
As model checking is emerging as an effective software validation method that
it is always desirable to have a dedicated model checker for domain specific
applications. While considering the development work that highly relies on both
domain and model checking knowledge, it is quite difficult and nontrivial to
build a dedicated model checker. Whereas in our PAT framework, we have this layered design and modularized
feature that allows our tool to be easily extended! The so-called
intermediate representation layer (IRL) which separates modeling from
verification, enables the underlying model checking algorithms (or other
analysis techniques like testing) to be shared by different modules. For
more details, please refer to section 5.1 PAT
Architecture.